Nuprl Lemma : mk-es0_wf 0,22

E:Type, eq:EqDecider(E), TV:(IdIdType), M:(IdLnkIdType), loc:(EId), k:(EKnd),
v:(e:Eeventtype(k;loc;V;M;e)), wa:(x:Ide:ET(loc(e),x)),
snds:(l:IdLnkE(Msg_sub(l;M) List)), sndr:({e:E| isrcv(k(e)) }E),
i:(e:{e:E| isrcv(k(e)) }||snds(lnk(k(e)),sndr(e))||), f:(E), prd:({e':Ef(e') }E),
cl:(EEProp), p:ESAxioms(E;T;M;loc;k;v;w;a;snds;sndr;i;f;prd;cl),
r:ESAtomAxiom{i:l}(T;i,k. kindcase(ka.V(i,a); l,t.M(l,t) )).
mk-es0(E;eq;T;V;M;loc;k;v;w;a;snds;sndr;i;f;prd;cl;p;r ES0 
latex


DefinitionsIdLnk, t  T, Id, f(a), Type, x,yt(x;y), x:AB(x), xt(x), kindcase(ka.f(a); l,t.g(l;t) ), AtomFree(T;x), Knd, x:AB(x), x:AB(x), <a,b>, b, ESAtomAxiom{i:l}(T;V), isrcv(k), True, T, P  Q, SqStable(P), {x:AB(x) }, Void, x:AB(x), Top, S  T, x.A(x), ESAxioms(E;T;M;loc;kind;val;when;after;sends;sender;index;first;pred;causl), Prop, A, , lnk(k), Msg_sub(l;M), ||as||, #$n, {i..j}, type List, eventtype(k;loc;V;M;e), EqDecider(T), Unit, , mk-es0(E;eq;T;V;M;loc;k;v;w;a;snds;sndr;i;f;prd;cl;p;q), ES0, P & Q
Lemmasit wf, deq wf, eventtype wf, int seg wf, length wf1, Msg sub wf, lnk wf, bool wf, not wf, ESAxioms wf, ESAtomAxiom wf, top wf, sq stable from decidable, decidable assert, assert wf, isrcv wf, Knd wf, atom-free wf, kindcase wf, Id wf, IdLnk wf

origin